T:Type, l1, l2:(T List).
fseg(T;l1;l2)
 ((||l1||  ||l2||) c (i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)]  T))) 

latex

ProofTree

Definitions	fseg(T;L1;L2), A  B, x:AB(x), P  Q, x:A. B(x), s = t, Type, t  T, type List, a < b, , ||as||, n - m, n+m, #$n, l[i], {x:A| B(x)} , , |g|, S  T, , A c B, x:A  B(x), i  j , P  Q, P & Q, P  Q, -n, Void, False, A, as @ bs, x:A. B(x), True, T, i  j < k, {i..j}, s ~ t, {T}, SQType(T), [car / cdr], x:A.B(x), Top, [], A List, firstn(n;as), nth_tl(n;as), {i...j}
Lemmas	append firstn lastn, select nth tl, length nth tl, list extensionality, nth tl wf, firstn wf, length wf nat, top wf, non neg length, cons one one, guard wf, select append back, int seg wf, append wf, true wf, squash wf, iff wf, rev implies wf, add functionality wrt eq, length append, member wf, fseg wf, le wf, length wf1, nat wf, select wf, fseg length